COMMENT ⊗   VALID 00013 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	PRA						ala  TAIT65FXR
C00009 00003	Numerical BMT  -- the theory -- ala BM
C00019 00004	Numerical BMT  -- the theory -- ala PRA
C00029 00005	Relating to <{k}-(nested)rec functions
C00031 00006	Consequences of  Number shell axioms (included in BM axioms)
C00032 00007	(1) With nested recursion the use of rank function is inessential
C00033 00008	In BM reducing LESSP to SUB1P
C00036 00009	Obtaining real shell from ideal shell
C00038 00010	Translation of Shell introduction into FM0 by characteristic function definition.
C00041 00011	Let 
C00043 00012	Parsons BUFFALO68+JSL#37[1972]
C00047 00013	% ____________________________________________________________________	%
C00048 ENDMK
C⊗;
PRA						ala  TAIT65FXR

Constants: 0, '(successor), function symbols
Variables: x,x1,y,z,...
Terms:	0, numeric variables, s', f[s1,...,sm]	(f m-ary)
Formulae: s1=s2, ¬A, A∧B, A->B, (A∨B, A<->B)

Axioms and rules:
A. (TAUT)	Truthfunctional tautologies
B. (EQUALITY)	x=x, x=y -> (A[x] -> A[y]), 
B1.(NUMBERS)	0≠x', x'=y' -> x=y
C. (INSTANTIATION) A[x]\\A[t]; 
D. (MP)  	A;A->B\\B
E. (MI)		A[0]; A[x] -> A[x'] // A[x]
F0. (Rules for introducing defined functions)
    (EDrule) 	f[X] <= t{G,X}		functions in G previously defined
    (PRrule) 	f[0,X] <= g[X]		g,h previously defined
             	f[y',X] <= h[y,X,f[y,X]]


Additional schema for recursion on << restricted to a

U{a,<<} (<<-UREC)
	f[0,X] = g[X]
	f[z',X,] = h[z',X,,f[r{<<}[z',X],X] ]
where r{<<}[y,X] = r[y,X]	if r[y,X]<<y<<a
		 = 0		OW

R{a,<<} (<<-NREC)
	f[0,X] = g[X]
	f[z',X] = t{f{<<,z'},z',X}
where
    t{f,u,V} is term with variables among u,V and at most f new function
and	
    f{<<,x}[y,Y]=f[if[y<<x<<a,y,0],Y]

U{<<},R{<<} without the restriction to a

x<y 
∀x<yA
p,p0,p1 pairing/projections

ith[x,i] is exponent of ith prime factor of x


Construction of orderings in PRA

a,b orderings  x <a y  for a[x,y]=0
  c=a*b lex ordering on pairs  
	x <c y iff [p1[x] <b p1 [y]] ∨ [p1[x]=p1[y] ∧ p0[x] <a p0[y]]
	
  a\b  finite maps b to a  think of numbers as alists 
    x  represents (...(ji,zi)...) if
    x+1=prod{i<r}(p/ji)zi with zi>0 and j0 >b j1 >b ...

    x <c y <-> ∃i≤y[ith[x+1,i] <a ith[y+1,i] ∧ 
		  ∀j≤y [i<bj -> ith[x+1,j]=ith[y+1,j]] ]


Family of pr relations w{n} (<{n})

w{0} = w
w{n+1} = w\w{n}

UREC{n} = PRA+<U{a,w{n}}>	(extend PR scheme,IND,etc. to UREC introduced fns)
NREC{n} = PRA+<R{a,w{n}}>

(also used to denote the class of functions definable)

Facts
UREC{n+1}=NREC{n}
NREC{1}=UREC{2}=Peter rec

Relation to BMA:  BMA is `conservative extension' of NREC{2}
How to see this
	(1) BMA <≡> NBM in the sense that 
		(1.1) NBM ⊂ BMA and 
		(1.2) can interpret BMA in NBM
		      code shells as numbers, 
		      shell functions as numeric functions
		      shell wfns via `count' function
		      this defines translation of terms which lifts to
			formulae and function definitions
		      If BMA |- A then NBM |- A#
	(2) Let NREC{1}← be extension of NREC{1} by adding T,F,IF,EQUAL 
		and extending function definitions in suitable fashion
	    (2.1) NREC{1}← is closed under BMrec 
	    (2.2) BMind is derivable in NREC{1}←
	    Thus NBM is essentially NREC{1}

What does this tell us
(1) The class of functions definable in NBM are just the Peter 
    multiple recursive functions
(2) A simple example of a function not definable is BMrec interpreter
	(it will be need full R{w{1}} recursion)
(3) Simple extension of NBM,BMA declaring w{n} to be WFns 

(4) Relation to formal systems with quantifiers
Let QPRA{n} be PRA with quantifiers and induction rule restricted to
formulae of quantifier depth ≤n

fεUREC{a,n} then f is definable  in QPRA{n}
(defining equations for f provable if QPRA{n} for suitable representing predicate)
e.g. there is F[x,y] st |- ∀x∃yF[x,y] and |- E{f}[i{y}F[x,y]]

ditto for NREC{a,n} QPRA{n+1}

If QPRA{n} |- ∀x∃yA[x,y] then least{n}A[x,n] is UREC{a,n} for some a

For n=2 there is a<<w\(w\w\) and a-rec f st A[x,fx] ∧ ∀y<fx¬A[x,y]
	and there is b<<w\w and b-*rec g ditto
and for such a,b,f,g HIR{2} |- defining equations
(note that for Pi{2} formulas IR{n} and IND{n} n>0 have same power)


Numerical BMT  -- the theory -- ala BM

Quantifier free theory of propositions of the form p=F/p≠F
Language
    Variables -- officially X0,X1,...
    Function symbols -- officially F{i,j} -the jth symbol of arity i- 0≤i,j

Remark:  Following the style of BM we will use upper case identifiers
for function symbols and specify the arity.
We will use BM names for function constants of the basic theory.
	
Terms -- s,t,u,...
~~~~~~~~~~~~~~~~~~
Variables
(F{i,j} t0 ... ti)

Formulas: a,b,...
~~~~~~~~~~~~~~~~~
t0=t1
¬a, a->b (a∧b; a∨b definable)


Metanotions
~~~~~~~~~~~
Substitution s, t/s

For a formula @A, a term t and a variable X, @A{X←t} is the result of
replacing all occurrences of X in @A by t (there need not be any).
@A{X0←t0,X1←,t1,...} denotes the parallel substitution


I. Logical axioms and rules.
   ~~~~~~~~~~~~~~~~~~~~~~~~~
A. (TAUT)	Truthfunctional tautologies
B. (EQUALITY)	Equality reasoning
C. (INSTANTIATION) a\\a/s
D. (MP)  	a;a->b\\b
    

Theory of IF,EQUAL,TRUE,FALSE
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


TRUE and FALSE	are 0-ary function symbols (say F{0,0} and F{0,1}).
We write T for (TRUE) and F for (FALSE).
In addition we have IF (3-ary) for the basic propositional function,
and EQUAL (2-ary) the basic relational function.


II: Propositional

	T≠F
	
	X≠F // (IF X,Y,Z) = Y
	X=F // (IF X,Y,Z) = Z

	X=Y // (EQUAL X,Y) = T
	X≠Y // (EQUAL X,Y) = F


Reduction to propositions of the form t0=t1,t0≠t1.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(NOT X Y) <- (IF X F T)
(IMPLIES X Y) <- (IF X (IF Y T F) T)
(OR X,Y) <- (IF X T (IF Y T F))
(AND X Y) <- (IF X (IF Y T F) F)

Propositions: p,q,r,...
A term, t, thought of as a proposition is an abreviation for t≠F .
If BMT |- t≠F we say t is a theorem

Facts:

(EQUAL X Y) = T ∨ (EQUAL X Y) = F
(NOT X) = T ∨ (NOT X) = F
(AND X Y) = T ∨ (AND X Y) = F
(OR X Y) = T ∨ (OR X Y) = F
(IMPLIES X Y) = T ∨ (IMPLIES X Y) = F

p = q <-> (EQUAL p q) = T
p=F <-> (NOT p) = T
[p≠F -> q≠F] <-> (IMPLIES p q) = T
[p≠F ∨ q≠F] <-> (OR p q) = T
[p≠F ∧ q≠F] <-> (AND p q) = T



Number Shell
~~~~~~~~~~~~
    r is NUMBERP
    const is ADD1 (1-ary)
    (btm) is (ZERO)
    ac1 is SUB1
    tr1 is (NUMBERP X1)
    dv1 is (ZERO)

We introduce the additional constants:
NUMBERP (1-ary), ZERO (0-ary), ADD1 (1-ary), SUB1 (1-ary) and LESSP (2-ary)
We write 0 for (ZERO), Num[X] for (NUMBERP X)≠F

III:  Number shell axioms (ala BM as propositional terms)

	(NOT (NUMBERP T))
	(NOT (NUMBERP F))

	(OR (EQUAL (NUMBERP X) T) (EQUAL (NUMBERP X) F))

	(NUMBERP 0)
	(NUMBERP (ADD1 X))
	(NUMBERP (SUB1 X))

	(NOT (EQUAL (ADD1 X) 0))

        (EQUAL (SUB1 (ADD1 X)) (IF (NUMBERP X) X 0))
	(IMPLIES (NOT (NUMBERP X)) (EQUAL (SUB1 X) 0) )
	(IMPLIES (NOT (NUMBERP X)) (EQUAL (ADD1 X) (ADD1 0)) )
	(EQUAL (SUB1 0) 0)

	(IMPLIES (AND (LESSP X Y) (LESSP Y Z)) (LESSP X Z))
	(IMPLIES (AND (NUMBERP X) (NOT (EQUAL X 0))) (LESSP (SUB1 X) X) )

	(EQUAL (EQUAL (ADD1 X) (ADD1 Y))
	       (IF (NUMBERP X)
		   (IF (NUMBERP Y) (EQUAL X Y) (EQUAL X 0))
		   (IF (NUMBERP Y) (EQUAL 0 Y) T) ) )

	(EQUAL (ADD1 (SUB1 X)) 
	       (IF (AND (NUMBERP X) (NOT (EQUAL X 0)))
		   X
		   (ADD1 0) ))

	(IMPLIES (AND (NUMBERP X) (NOT (EQUAL X 0)))
		 (EQUAL (ADD1 (SUB1 X)) X) )



Measured lexicographic orderings <{k,m1,...mk}
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Let m1...mk be l-ary functions then

	[Y1 ... Yl]<{k,(m1...mk)}[X1 ... Xl] <::>  
		[(m1 Y1...Yl) ... (mk Y1...Yl)] <k [(m1 X1...Xl) ... (mk X1...Xl)]

    where
	[Y1 ... Yk] <k [X1 ... Xk] <::>  
		(IF (LESSP Y1 X1) T
	        (IF (EQUAL Y1 X1) 
		    (IF (LESSP Y2 X2) T
			............

		    (IF (EQUAL Yk-1 Xk-1) 
			(IF (LESSP Yk Xk) T F))


Ranked WFOs <{m,r}
~~~~~~~~~~~~~~~~~~
    Let m be n-ary function, r a WFO

	[Y1 ... Yn]<{m,r}[X1 ... Xn] <::>  (r (m Y1...Yn) (m X1...Xn))

IV{r0,r1}: rule for introduction of WFOs (in presence of CONS shell)
	   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Let:
(a) f be `new' 2-ary function symbol 
(b) r0,r1 be WFOs 

Introduce f as WFO with defining axiom
(f P1 P2) = (OR (r0 (CAR P1) (CAR P2)) 
		(AND (EQUAL (CAR P1 P2)) (r1 (CDR P1) (CDR P2)) ) )

IV'{r0,r1}: rule for introduction of WFOs (in Numerical theory)
	   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Let:
(a) f be `new' 2-ary function symbol 
(b) r0,r1 be WFOs 

Introduce f as WFO with defining axiom
(f P1 P2) = (OR (r0 (CAR P1) (CAR P2)) 
		(AND (EQUAL (CAR P1 P2)) (r1 (CDR P1) (CDR P2)) ) )



f-free
~~~~~~
#[f,t]
~~~~~~
f,n,t[f,x_]-machine {(q{i} t{i,1} ... t{i,n} ) | 1≤i≤#[f,t]}
~~~~~~~~~~~~~~~~~~~
    f an n-ary function symbol, t a term, 
    qi the conjunction of the f-free terms governing (f t{i,1} ... t{i,n}) in t

V{f,t,m,r}: rule for introduction of function definitions.
             ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Let:
(a) f be `new' n-ary function symbol 
(b) x1...xn distinct variables
(c) t a term constructed from old function symbols, f, and x1...xn
(d) for 1≤i≤k; (f t{i,1}...t{i,n}) the occurrences of f in t
(e) for 1≤i≤k  qi the f-free term governing (f t{i,1}...t{i,n}) in t
(f) r a WFO
(g) m an n-ary function symbol
(e) for 1≤i≤k  s{i} the substitution {x1<-t{i,1}...xn <- t{i,n}}

If

  BMTheorem (IMPLIES qi (r (m x1 ... xn)/s{i} (m x1 ... xn) ))  for 1≤i≤k

then we may introduce the function f with the defining axiom 

  BMDefinition (f x1 ... xn) = t





VI{m,r}: Rule for Rank-Induction on WFO
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Let:
(a) p be a term		(the proposition to be proved)
(b) r a WFO
(c) m an n-ary function symbol
(d) x1,...xn distinct variables
(e) q1,...qk terms
(f) h1,...hk positive integers
(g) for 1≤i≤k; 1≤j≤hi  s{i,j} are substitutions 
(h) q0 <::> (AND (NOT q1)...(NOT qk))

If

  BMTheorem (IMPLIES qi (r (m x1 ... xn)/s{i,j} (m x1 ... xn) ))  for 1≤i≤k; 1≤j≤hi

  BMTheorem (IMPLIES q0 p)

  BMTheorem (IMPLIES (AND qi p/s{i,1} ... p/s{i,hi}) p)  for 1≤i≤k

then 

  BMTheorem p

Numerical BMT  -- the theory -- ala PRA

Quantifier free theory  of `N + {T,F}


Language
    Variables -- officially X0,X1,...
    Function symbols -- a symbols for functions of each arity ≥0
	including those given below and additional symbols introduced
	according to the function definition rule.

    Propositional functions --
        TRUE:0,TRUEP:1
	FALSE:0,FALSEP:1
	IF:3,EQUAL:2

    Numerical functions --
	ZERO:1,
        NUMBERP:1,ADD1:1,SUB1:1,LESSP:2

V,V0,... will stand for variables
f,g,h will stand for function symbols 

Remark:  Following the style of BM we will use upper case identifiers
for function symbols and specify the arity.
We will use BM names for function constants of the basic theory, but
terms and other expressions will be written in more standard mathematical
notation.  
	
Terms -- t,t0,t1..	
~~~~~~~~~~~~~~~~~~
Variables
f[t1,..,tk]  if f has arity k

Notation: f[t] will also be written f t when not ambiguous

Formulas -- @A,@B,...
~~~~~~~~~~~~~~~~~~~~~
t0=t1
¬@A, @A->@B @A∧@B @A∨@B


Metanotions
~~~~~~~~~~~
Substitution s is given by a set of assignments {...,Vi<-ti,...}.

For a formula @A (term t) and substitution s, @A/s (t/s) 
is the result of simultaneously replacing all occurrences of Vi in @A (t) 
by ti (there need not be any) for each assignment in s.

For a term t the corresponding proposition is defined as t≠FALSE[]
(e.g. t≠F see below)


I. Logical axioms and rules.
   ~~~~~~~~~~~~~~~~~~~~~~~~~
A. (TAUT)	Truthfunctional tautologies
B. (EQUALITY)	Equality reasoning
C. (INSTANTIATION) @A // @A/s
D. (MP)  	@A; @A->@B // @B
    

Propositional theory
~~~~~~~~~~~~~~~~~~~~
Abbreviations:
    T :: TRUE[]
    F :: FALSE[].

Axioms:

    T≠F
     
    X≠F -> IF[X,Y,Z] = Y
    X=F -> IF[X,Y,Z] = Z

    X=Y -> EQUAL[X,Y] = T
    X≠Y -> EQUAL[X,Y] = F


Number domain 
~~~~~~~~~~~~~
Abbreviations:
    0 :: ZERO[]
    1 :: ADD1[0] etc.
    Num[X] :: NUMBERP[X]≠F 
    X < Y :: LESSP[X,Y]≠F
    Zero[X] :: X=0 ∨ ¬Num[X]

Axioms:

	NUMBERP[X]=T ∨ NUMBERP[X]=F
	¬Num T 
	¬Num F 

	Num 0 
	Num[ADD1 X]
	Num[SUB1 X]

	ADD1[X]≠0
	SUB1[0]=0
        Num X ∧ Num Y ∧ ADD1 X = ADD1 Y -> X=Y
	¬Num X -> SUB1[X]=0
	¬Num X -> ADD1[X]=ADD1[0]
	Num X -> SUB1[ADD1 X]=X; 
	¬Zero[0] -> ADD1[SUB1 X] = X

	LESSP[X,Y]=T ∨ LESSP[X,Y]=F

	Zero Y -> ¬X < Y
	¬Zero Y ∧ Zero X -> X < Y
	¬Zero Y ∧ ¬Zero X -> X < Y <-> SUB1[X] < SUB[Y]

 	X<Y ∧ Y<Z -> X<Z
 	¬Zero X -> SUB1[X]<X


Notation for measured lexicographic ordering based on <:
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For terms t1,...,tk,t1',...tk' 

(t1,..,tk) <{k} (t1',...,tk') is defined inductively by

t1 <{1} t1' <-> t1 < t1'

(t1,..,tk) <{k} (t1',...,tk') <-> 
	t1 < t1' ∨ t1=t1' ∧ (t2,..,tk) <{k-1} (t2',...,tk')	if k>1

if m1...mk is list of n-ary function symbols we write 
m_[t1,...tn] for the list (m1[t1,...,tn],...,mk[t1,...,tn])


Rule for Induction (k-Measured LESSP with l cases)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Let:
(a) @P be a formula	(the proposition to be proved)
(b) x1,...xn be distinct variables
(c) m1...mk n-ary function symbols (m_ interpreted as above)
(d) @Qi 1≤i≤l formulae	(describing the l non-base cases)
(e) for 1≤i≤l; 1≤j≤hi  s{i,j} is a substitution
	(the jth instance of IH in ith case; hi the number of such instances)
(f) @Q0 <::> ¬@Q1 ∧ ... ∧ ¬@Ql

then the induction rule is 

	@Qi ->[m_[x1...xn]/s{i,j}] <{k} m_[x1 ... xn] ]  for 1≤i≤l; 1≤j≤hi
	@Q0 -> @P
	@Qi ∧ @P/s{i,1} ∧ ... ∧ @P/s{i,hi} -> @P  for 1≤i≤l
	_______________________________________________________

		 	 @P


Notation for function definition
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We define a notion which is useful in analyis of functions defined
by recursion equations based on conditional expressions.
The idea is given a term t and an occurrence of a subterm f[t_]
we want a list of terms Q, `governing' the occurrence of f in t with
the property that if @Q is the conjunction of the corresponding propositions 
then 
	[@Q -> f[t_]=w] -> t = t{f[t_]←w]

where w is a new variable and the substitution is just for the particular
occurrence of f[t_].

The determination of Q is base on the following property of IF:

	[X≠F -> t0=w]  -> IF[X,t1[w],t2]=IF[X,t1[t0],t2]


In particular given a term t, a function symbol f and a list of terms Q
the list of occurences of subterms of the form f[..] in t paired with
the f-free terms governing that occurrence is called the f-machine for
t relative to Q, written mach{f,t,Q} and is defined by induction on 
the construction of t as follows:

If t is f[t1,..,tn] then mach[f,t,Q]= <(f,Q)> * mach1 *...* machn
	where machi=mach[f,ti,Q]

If t is g[t1,..,tk] (g not f or IF) then mach[f,t,Q]=  mach1 *...* machk
	where machi=mach[f,ti,Q]

If t is IF[t0,t1,t2] then 
    mach[f,t,Q]= mach[f,t0,Q] * mach[f,t1,Q1] * mach[f,t2,Q2]
where 
    Q1 = (t0,Q,) 	if t0 is f-free 
       = Q		OW
    Q2 = (NOR[t0],Q,) 	if t0 is f-free 
       = Q		OW

We for (Qi,f[t{1,i}) in mach[f,t,<>] let @Qi denote the conjunction of
corresponding propositions and call @Qi the f-free test governing the
corresponding occurrence of f in t.


Rule for introduction of function definitions.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Let:
(a) f be `new' n-ary function symbol 
(b) x1...xn distinct variables
(c) t a term constructed from old function symbols, f, and x1...xn
(d) for 1≤i≤k;  f[t{i,1}...t{i,n}] the occurrences of f in t
(e) for 1≤i≤k  @Qi the f-free test governing  f[t{i,1}...t{i,n}] in t
(f) m1...mk n-ary function symbols
(g) for 1≤i≤k  si the substitution {x1 <- t{i,1}...xn <- t{i,n}}

If   |-  @Qi -> m_[x1,...,xn]/si <{k} m_[x1,...,xn]] for 1≤i≤k

then we may introduce the function f with the defining axiom 

     f[x1 ... xn] = t


Relating to <{k}-(nested)rec functions
Assume stnd encoding of <{k} in `N

let beta{k}[z,x] = z if z <k x
              =	0 OW

phi[0,y] = psi[y]
phi[x',y] = chi[x',y,phi[beta{k}[delta[x',y],x'],y] ]

phi#[x,y] = psi#[y]	if Zero[x]
phi#[x,y] = chi[x,#y,phi[beta{k}[delta[x,#y],x],#y]]	if ¬Zero[x]
          = chi[x,#y,phi[beta#{k}[delta#[x,y],x],#y]]	
          = chi#[x,y,phi#[beta#{k}[delta#[x,y],x],y]]	


Assume LESSP{k} has been introduced (as PR function expressing <k#)
Then beta{k} is introduced by

B{k}[Z,X] <= IF[LESSP{k}[Z,X],Z,0]

Let mi[Z]=pi[i,k,Z] for 1≤i≤k the ith projection of k tuple then

¬Zero[X] -> m_[B{k}[Z,X]] <{k} m_[X]


Assume psi#,chi#,delta# have been introduced as g,h,d then
phi# is introduced as f by

f[X,Y] = IF[ZEROP[X],g[Y],h[X,Y,f[B{k}[d[X,Y],X],Y]]

using the fact given above.



Consequences of  Number shell axioms (included in BM axioms)

¬Num X -> SUB1[ADD1 X]=0
by
    follows from above  Num 0 and ¬Num X -> ADD1[X]=ADD1[0]
Num X -> X<ADD1[X]	from  Num X  ∧ X≠0 -> SUB1[X]<X 


Num X ∧ ¬Num Y ∧ ADD1 X = ADD1 Y -> X=0
¬Num X ∧ Num Y ∧ ADD1 X = ADD1 Y -> 0=Y
by
	Num 0; ¬Num X -> ADD1[X]=ADD1[0];
        Num X ∧ Num Y ∧ ADD1 X = ADD1 Y -> X=Y

¬Num X ∨ X=0 -> ADD1[SUB1 X] = ADD1[0]
by
	¬Num X -> SUB1[X]=0; SUB1[0]=0; 


(1) With nested recursion the use of rank function is inessential

reduction to pure nested recursion (ala TAIT61NESTED#5

suppose f[x1,...,xn] = t[x1,..,xn,...f[tj1,...tjn]...]

where qj -> r[tj1,...tjn] << r[x1,...,xn]   (from machine for f, qj,tji involve x_)
<< standard with 0 least element

define F[m,x_] = if{m=0,d[x_],t*[m,x_]}  where 
    (1) d[x_] is f[x_] for r[x_] = 0
    (2) t* it obtained by replacing f[tj_[x_]] by F[{r[tj_ x_]|<<,m}, tj_]
then 
    f[x_] = F[r[x_],x_] and the definition of F is nested-<<-recursive
	(need to check details)


In BM reducing LESSP to SUB1P

Suppose f[x_]=t[f,x_] is accpeted BM definition via m,r{LESSP}

(1) assume r is LESSP 

define f0[n,x_]=if{ZEROP[n],0,t[λx_f0[n-1],x_]} (PR on n)
show ∀k,x_ f0[m[x_]+k+1,x_]=f0[m[x_]+1,x_]
define f1[x_]=f0[m[x_]+1,x_]
then f1[x_]=t[f1,x_]

use m[s[x]]<m[x_] for recursive calls so by 
f1[s[x_]]=f0[m[s[x_]]+1,s[x_]]=f0[m[x_],s[x_]]

to show ∀k,x_ f0[m[x_]+k+1,x_]=f0[m[x_]+1,x_]

for k=0 trivial
assume ∀x_ f0[m[x_]+k+1,x_]=f0[m[x_]+1,x_]
consider 
f0[m[x_]+k'+1,x_]=t[λx_.f0[m[x_]+k+1,x_],x_]
within t have f0[m[x_]+k+1,s[x_]] under hyp[s][x_]
while for
f0[m[x_]+1,x_]=t[λx_.f0[m[x_],x_],x_]
within t have f0[m[x_],s[x_]] under hyp[s][x_]

need 
within t have f0[m[x_]+k+1,s[x_]]=f0[m[x_],s[x_]] under hyp[s][x_]



In BM reducing SUB1P to LESSP

suppose q[x] -> m[t[x]] <{w,k} m[x]	for some lex{wfn} and measure m=m1..mk

define m'=m1'...mk' where mj'[y]=count[mj[y]]
 
then q[x] -> m'[t[x]] <{k} m'[x]

proof -- (induction on lex complexity)

for k=0 trivial(a<{w,0}b always false)

m[t[x]] <{w,k} m[x] <-> m1[t[x]] <{w,1} m1[x] ∨
		        m1[t[x]] = m1[x]  ∧  {m2...mk}[t[x]] <{w,k-1} {m2...mk}[x] 

In the < case m1[t[x]] = acj[m1[x]] for some suitable accessor
thus count[m1[t[x]]] < count[[m1[x]]]
and m'[t[x]] <{k} m'[x]

= case follows by IH

Obtaining real shell from ideal shell

Assume TRUE,FALSE,ADD1 shells are initially added
PLUS defined

Add to the functions introduced with a shell
	"cnt 1-ary function symbol
Let c be the count function for the previous shell (ZERO1 of no previous shell)
Assume n > 0 and shell has btm

(8) ("cnt X) <- (IF ("r X) 
   		    (IF (EQUAL X ("btm)) 
			0 
			(ADD1 (PLUS ("cnt ("ac1 X))...("cnt ("acn X)))) )
   		    (c X) ) 

For n=0 replace (ADD1 (PLUS ("cnt ("ac1 X))...("cnt ("acn X)))) by 0
For shell without btm replace (EQUAL X ("btm)) by F
(and simplify the definition of "cnt)

thus at any stage the most recent count function gives the same 
value as BM count for data in existing shells.
It will give 0 for other whereas BMcount not defined

Notice that "cnt is introduced according to the definition principle
using either (6) or (6*) for the definition of "wfn


If (6*) is taken for introducing wfns then
ideal shell + cnt coutains LESSP and all real shell measure functions

If (6) is taken for introducing wfns then

Translation of Shell introduction into FM0 by characteristic function definition.

The most direct translation seems to be to define (decidable) classes
of shell and botttom tags, and define recognizers (as total functions) 
by PR-recursion and then define constructors that coerce.  The
accessors are then just simple projections or defaults.

Shell tags -- (`s,j)
Bottoms -- (`b,j)

System of recognizer,constructor,accessor,bottom names (for meta use)
R{j},cons{j},ac{j,1}...ac{j,n{j}},btm{j}
tr{j,i} will stand for the partial term representing tri
dv{j,i} the translation of dvi

a  type restriction tri is translated as follows --
Xi -> xi
rk[xi] --> R{k}<xi>
TRUE[] --> `true
TRUE[] --> `false
IF[tr0,tr1,tr2] --> if{tr0~,tr1~,tr2~}

R{j} is defined as the solution (note R{j} may appear in tr{j,i} some i)

without bottom
R{j}<x> ← and{eq[len[x],n+1],
	    eq[elt[0,x],(`s,j)],
	    tr{j,1}[elt[1,x]],
		...
	    tr{j,n}[elt[n,x]] }

with bottom
btm{j}=(`b,j)
r{j}x ← or{eq[x,btm{j}]
	    and{eq[len[x],n+1],
		eq[elt[0,x],(`s,j)],
		tr{j,1}[elt[1,x]],
		    ...
		tr{j,n}[elt[n,x]] }}

and{y1...yn} <::> if{y1,...,if{yn,T,F},...,F}
note that ∀x∃y:{T,F} R{j}[x]=y is provable in FM0 by complete induction on V
as tr{j,i}z is term composed of total functions or R{j}[x]

dfv{j,i}[x] <- if{tr{j,i}[x],x,dv{j,i}}
cons{j}[x1...xn] <- <(`s,j,n) dfv{j,1}x1...dfv{j,n}xn >
ac{j,i}x <- if{r{j}x,elt[i,x],dv{j,i}}

Let 
TR{j,i}={xi | tri[xi]}
R{j}={x | r{j}x = T}

x1:TR1 ∧...∧ xn:TRn -> <(`s,j,n) x1...xn>:R{j}

The shells are a collection of decidable classes
sub class of V* -{0} with elt[0,x] a shell-tag

to define R{j} we define R{j},-R{j} simultaneously

in terms of R{l},-R{l} for l<j (recall that trs translate to boolean comb of Rs)

tr(x)  TR	-TR	tr(x)=T <-> x:TR  tr(x)=F <-> x:-TR

T	`V	`MT
F	`MT	`V
r{l}x	 R{l}	-R{l}

if{tr0 tr1 tr2}	 TR0∧TR1 ∨ -TR0∧TR2


Assume simplified disjunctive normal form -- 
	B1 ∨...∨ Bp ∨ C1 ∨...∨ Cq ∨ D1 ∨...∨ Dm

where each clause is conjunction of Rs, -Rs
(`V is omitted from conjunct and conjuncts wwth `MT or both R{l},-R{l} are omitted)

where Bi's don't contain R{j},-R{j}, Ci's contain R{j}, Di's contain -R{j}

or TR is `V

(TR cannot reduce to `MT  by hyp (c))

and the constraint n TR,-TR holds hereditarily

and x:R{l} <-> r{l}x=T, x:-R{l} <-> r{l}x=F holds hereditarily

for R,-R defined from TR,-TR via FIG

With regard to induction on shells -- the count function is FM0 definable.
Using recognizers, and PR-induction we get wfn-induction on 
shells so far.

Parsons BUFFALO68+JSL#37[1972]
Let Z0 be theory of <=,0,',<ef{i}>> in 1st order PC (with quantifiers)
    EQax;ALG{0,'};{DEFeqns[ef{i}]| ef elementary};IR{Open}

Two families of Z0-equivalent theories based on additional schemata for 
    Induction 
    AS (finite separation)
IA'{n}-IR'{n}-IA{n}-IA{Pi,n}-IA{Si,n}-AS{n}-AS'{n}-AS{Pi,n}
IR{n}-IR{Si,n}

Other results about power of 
    FAC (finite axiom of choice)
    M  (finite max)
    
Pi{n+1} sentences provable in (Z0+) IA{n} are provable in IR{n}
Pi{n+1} sentences provable in (Z0+) IA{Pi,n} are provable in IR{Pi+,n}
	PHI[x] ~~ A->B[x] with A,B Pi{n}

Let T be QF-theory of PRFT (ala spector or tait)
For a:t, b:(0,t;t) (and suitable interpretation of ==)
R{t}ab0 == a;  R{t}abx' == bx(R{t}abx)
D{c}ab0 == a;  D{c}abx' == b

For closed terms P:(t1..tk;t) Q:(t1...tk,0,t->t) and ai:ti
introduce f:(t1..tk0;t) by PR{t1..tk;t}	
fa1..ak0 == Pa1...ak;	fa1..akx' == Qa1...akx(fa1...akx)

T{n} is T with R{t} only for t of level≤n
T*{n} is T with {R{t} | level[t]<n}+{PR{t1...tk,t} | level[ti]≤n,level[t]=n}
Let A-' be negative+Godel tranlation form Z0 to T; 
B% translation from T to Z0 interpreting functionals as HEOs
Write T |= A-' for A-' satisfiable in T etc..

IA'{n+1} has G\"odel functional interpretation in T{n}
IR{Pi+,n+1} has G\"odel functional interpretation in T*{n}
If T{n} (T{n} n≠0; T'{0}) |= A-'  then 
    IA{Pi,n+1} (IR{Pi+,n+1}, IR{Si,1}+FAC{0}) |- [A-']%
Also IR{Si,1}+FAC{0} |- A ≡ [A-']%

Thus
     T{n} |= A-'  iff   IA{Pi,n+1} |- A
    T*{n} |= A-'  iff  IR{Pi+,n+1} |- A  (n≠0)
    T'{0} |= A-'  iff  IR{Si,1}+FAC{0} |- A  

NOTAMS#13[1966]
<< PRWO on `N of Sch\"utte[#13] (|<<| = Gamma0+1)
Let om[0]=w; om[n+1]=w\om[n]; 
HIR{n} (HA|IR{n} rather than PA|IR{n})
Fix n and a<om{n} <<a lam{x,y}{x<<y<<a}

f : <<a-rec (<<a*-rec) then HIR{n} (HIR{n+1} |- defining equations for f 
	(for suitable representing predicate)

IR{n} |- ∀x∃yA[x,y] then least{n}A[x,n] is <<a-rec for some a<om{n}
IR{n} |- ∀x∃yA[x,y] then HIR{n} |- ∀x∃yA[x,y]

JSL#33[1971]
IA{n} |- A then A has NCI interpretation by functionals a-rec for some a<om{n}
The same functions are <<a-rec a<om{n+1} as are PR of degree≤k
(recursion schema restricted to level k?)


SchwictenbergLC73

% ____________________________________________________________________	%